\begin{tabbing}
$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:event\_system\{i:l\}, $x$:Id, $e$:es{-}E(${\it es}$).
\\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex]es{-}locl(${\it es}$; ${\it e'}$; $e$)
\\[0ex]$\Rightarrow$ ($\neg$(es{-}after(${\it es}$; $x$; ${\it e'}$) = es{-}when(${\it es}$; $x$; ${\it e'}$) $\in$ $T$))
\\[0ex]$\Rightarrow$ es{-}le(${\it es}$; ${\it e'}$; (last change to $x$ before $e$)))
\-
\end{tabbing}